(declare-fun _substvar_62_ () Real)
(declare-fun _substvar_155_ () Bool)
(declare-const r4 Real)
(declare-const r5 Real)
(declare-const r6 Real)
(push)
(assert _substvar_155_)
(assert (< 0.0 _substvar_62_ 904377.0 r5 (/ r6 (/ r4 0.798208961))))
(check-sat)
(declare-const v0 Bool)
(declare-const v11 Bool)
(declare-const r0 Real)
(declare-const r6 Real)
(declare-const v22 Bool)
(declare-const r10 Real)
(push)
(assert (or (= r10 (/ r0 (+ 0.3655876 203356609.0 r0 r0 r6)) r0 86.0 r0) v22 (<= 13.0 13.0 r6 203356609.0 r0)))
(assert (or (= r10 (+ 0.3655876 203356609.0 r0 r0 r6) r0 86.0 r0) v0 v11 v0))
(check-sat)
